T:Type, as:(T List). (null(as))  (as = []) 

latex

Definitions	prop{i:l}, t  T, P  Q, P  Q, P  Q, True, if b then t else f fi , ff, tt, null(as), b, P  Q, x:A. B(x), False, A
Lemmas	false wf, true wf, cons neq nil